postulate
  @lock _ : Set
